Inference at * 1 
Iof proof for Lemma p-compose wf:



1. A : Type
2. B : Type
3. C : Type
4. g : A(B + Top)
5. B(C + Top)
6. x : A
7. (can-apply(g;x))
  g(x)  (C + Top) 

latex

 by ((MoveToConcl (-1)) 
CollapseTHEN (((Unfold `can-apply` ( 0)) 
CollapseTHEN (((((
CGenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto))) 
CCollapseTHEN (((D (-2)) 
CCollapseTHEN (((
CCReduce 0) 
CCollapseTHEN (Auto)))))))))) 

latex

CC.

Definitions	can-apply(f;x), inl x , True, b, P  Q, Decision, , left + right, f(a), inr x , Top, Type, A, x:A. B(x), x:AB(x), False, t  T, s = t
Lemmas	top wf, member wf, true wf, not wf, false wf